<html>
<head><meta charset="utf-8"><title>recursive solver · wg-traits · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/index.html">wg-traits</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html">recursive solver</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="188374760"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/188374760" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#188374760">(Feb 17 2020 at 12:38)</a>:</h4>
<p>I'm still working on the writeup here -- on vacation in New York City this weekend :) -- but I wanted to drop a note to <a href="https://gist.github.com/nikomatsakis/bfbdbe588d6fc61ecb09e3b51847fb7c" target="_blank" title="https://gist.github.com/nikomatsakis/bfbdbe588d6fc61ecb09e3b51847fb7c">this gist</a> where I'm leaving some notes about my thoughts on returning to a recursive solver for chalk and how it might help with the associated type ambiguity problem. (I didn't get to that last part yet, really ;)</p>



<a name="188374777"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/188374777" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#188374777">(Feb 17 2020 at 12:38)</a>:</h4>
<p>will post some notes in it when I get chance</p>



<a name="188813573"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/188813573" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#188813573">(Feb 22 2020 at 11:35)</a>:</h4>
<p>I pushed the remaining notes here -- sorry again for not catching up on the other topics, will do so on Monday &lt;3</p>



<a name="188814373"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/188814373" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#188814373">(Feb 22 2020 at 11:57)</a>:</h4>
<p>The connection between the recursive solver and the associated type ambiguity problem is not clear to me -- would it not be possible to implement the priority logic in the SLG solver?</p>



<a name="188820591"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/188820591" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#188820591">(Feb 22 2020 at 14:55)</a>:</h4>
<p>Also, I don't really understand <em>how</em> the solver is supposed to work and is different than the current</p>



<a name="188821249"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/188821249" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#188821249">(Feb 22 2020 at 15:13)</a>:</h4>
<p><span class="user-mention" data-user-id="232957">@Jack Huey</span> my understanding is that the difference is that <em>each subgoal</em> returns either a unique solution or 'ambiguous', while in the current solver a subgoal can return multiple solutions and only the top-level turns that into ambiguity.</p>
<p>I guess that's the connection to the associated type ambiguity -- the SLG solver might have to return both possible solutions to the type normalization (the real one and the placeholder) for correctness, while the recursive solver can't do that anyway. But it's not clear to me that that's really the case for SLG -- with my naive understanding of how it works, I can imagine it stopping after it has found a solution with the 'high-priority' subgoal and skipping the equivalent 'low-priority' one (I guess that's maybe similar to other solutions proposed in the past?)</p>



<a name="188821360"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/188821360" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#188821360">(Feb 22 2020 at 15:16)</a>:</h4>
<p>Ah, that makes sense I think.</p>



<a name="188821447"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/188821447" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#188821447">(Feb 22 2020 at 15:19)</a>:</h4>
<p>For SLG, what you're talking about is the "cut" idea <span class="user-mention" data-user-id="116009">@nikomatsakis</span> was talking about on the issue thread. I think it <em>might</em> be possible to conditionally generate the fallback if the normalization clause can't be generated. But it doesn't align really well with the idea of "generating all possible answers"</p>



<a name="188947665"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/188947665" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#188947665">(Feb 24 2020 at 17:36)</a>:</h4>
<p>So, <span class="user-mention" data-user-id="129457">@Florian Diebold</span>, I think maybe you already worked your way to my answer, but to clarify. The connection I see is this. In the "recursive" solver, we fully compute <strong>a single answer</strong> from each query and we don't do any dependent work until that answer is ready (with the exception of cycles). This makes it (relatively) easy to allow some answers to "override" others before they propagate out.</p>
<p>I'm not sure how to do that in the "non-recursive" setup -- it seems to me it would be much harder.</p>
<p>That said, the other reason thing that I think may be useful about the recursive solver is precisely that it may use less time/memory, basically for the same reason, though at the cost of completeness (as I mentioned). </p>
<p>I'm not really sure which approach is best, idealy we'd have some room to experiment with both.</p>



<a name="190020506"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190020506" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190020506">(Mar 08 2020 at 17:07)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> <span class="user-mention" data-user-id="232957">@Jack Huey</span> I've revived the old recursive solver in a branch <a href="https://github.com/flodiebold/chalk/tree/recursive-solver" target="_blank" title="https://github.com/flodiebold/chalk/tree/recursive-solver">here</a>. It's passing a lot of tests, but also failing a few; I haven't looked into the test failures though</p>



<a name="190020712"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190020712" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190020712">(Mar 08 2020 at 17:13)</a>:</h4>
<p>just from a quick glance, it's probably failing the coinductive tests</p>



<a name="190020781"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190020781" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190020781">(Mar 08 2020 at 17:15)</a>:</h4>
<p>no coinductive tests are failing, but I only changed the default solver choice, so the later ones which specify the slg solver parameters still run with that one</p>



<a name="190020825"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190020825" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190020825">(Mar 08 2020 at 17:16)</a>:</h4>
<p>here are the failing tests:</p>
<div class="codehilite"><pre><span></span>failures:
    test::auto_traits::auto_semantics
    test::coherence::nonoverlapping_assoc_types
    test::coherence_goals::fundamental_types
    test::cycle::overflow
    test::existential_types::dyn_Foo_Bar
    test::existential_types::dyn_binders_reverse
    test::misc::subgoal_abstraction
    test::misc::subgoal_cycle_inhabited
    test::misc::subgoal_cycle_uninhabited
    test::projection::normalize_under_binder_multi
    test::projection::projection_from_env_slow
    test::unify::unify_quantified_lifetimes
    test::wf_lowering::assoc_type_recursive_bound
    test::wf_lowering::higher_ranked_cyclic_requirements
</pre></div>



<a name="190021304"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190021304" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190021304">(Mar 08 2020 at 17:31)</a>:</h4>
<p>ohh</p>



<a name="190077752"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190077752" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190077752">(Mar 09 2020 at 14:59)</a>:</h4>
<p>oh, interesting</p>



<a name="190077773"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190077773" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190077773">(Mar 09 2020 at 14:59)</a>:</h4>
<p>I was starting a branch re-implementing the recursive solver</p>



<a name="190077964"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190077964" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190077964">(Mar 09 2020 at 15:01)</a>:</h4>
<p>but maybe starting from the old code is a good idea, indeed</p>



<a name="190078168"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190078168" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190078168">(Mar 09 2020 at 15:02)</a>:</h4>
<p>You might be able to easily reimplement it from scratch; I thought I'd probably get farther this way ;)</p>



<a name="190080220"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190080220" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190080220">(Mar 09 2020 at 15:21)</a>:</h4>
<p><span class="user-mention" data-user-id="129457">@Florian Diebold</span> maybe but I suspect this would be faster :)</p>



<a name="190080225"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190080225" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190080225">(Mar 09 2020 at 15:21)</a>:</h4>
<p>skimming the code now</p>



<a name="190080313"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190080313" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190080313">(Mar 09 2020 at 15:22)</a>:</h4>
<p>side note that I was wondering whether having a chalk-engine crate with callbacks into chalk-solve was a real win</p>



<a name="190080335"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190080335" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190080335">(Mar 09 2020 at 15:22)</a>:</h4>
<p>given that rustc would integrate at the chalk-solve level, and not chalk-engine level</p>



<a name="190080448"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190080448" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190080448">(Mar 09 2020 at 15:23)</a>:</h4>
<p>one difference is that it invokes <code>program_clauses_for_goal</code> to get the callbacks, which is going to include the results from the environment; the old logic of finding <code>env_solution</code> prog_solution` needs to be updated</p>



<a name="190080508"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190080508" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190080508">(Mar 09 2020 at 15:23)</a>:</h4>
<p>the main point of that logic was to rationalize some of rustc's more "curious" behavior</p>



<a name="190080874"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190080874" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190080874">(Mar 09 2020 at 15:26)</a>:</h4>
<p>I think the call to <code>program_clauses_for_goal</code> also doesn't deal correctly with bound vars. It's causing the <code>dyn_Foo_Bar</code> test to fail. I'm just calling <code>program_clauses_for_goal</code> with the canonicalized value, and I don't think it's handling that correctly</p>



<a name="190224618"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190224618" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190224618">(Mar 10 2020 at 21:04)</a>:</h4>
<p><span class="user-mention" data-user-id="129457">@Florian Diebold</span> btw are you hacking on this stuff? do you want me to take a look?</p>



<a name="190228247"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190228247" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190228247">(Mar 10 2020 at 21:35)</a>:</h4>
<p>I am hacking on it a bit, I'll see how far I get</p>



<a name="190289124"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190289124" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190289124">(Mar 11 2020 at 14:46)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> I'm wondering if you have an idea how to integrate the caching for the recursive solver with Salsa, though. In principle it seems straightforward, but in practice I think the cycle handling makes it more complicated</p>



<a name="190336248"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190336248" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190336248">(Mar 11 2020 at 21:55)</a>:</h4>
<p><span class="user-mention" data-user-id="129457">@Florian Diebold</span> I do have thoughts, but it involves modifying salsa somewhat</p>



<a name="190336269"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190336269" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190336269">(Mar 11 2020 at 21:55)</a>:</h4>
<p>I may try to pull in some of your changes from branch and do some tinkering, but I think you should go on changing</p>



<a name="190336343"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190336343" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190336343">(Mar 11 2020 at 21:56)</a>:</h4>
<p>I don't think there's a "perfect answer" when it comes to salsa -- i.e., I'm not sure what mechanism we can add that can't be misused -- but it should be possible to make some "opt-in" way for salsa to accept cyclic queries like this one</p>



<a name="190336357"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190336357" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190336357">(Mar 11 2020 at 21:56)</a>:</h4>
<p>perhaps with a few "modes" of operation -- the "re-execute until a consistent response is reached" mode is not bad (i.e., "Tabled prolog execution")</p>



<a name="190842866"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190842866" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190842866">(Mar 17 2020 at 12:56)</a>:</h4>
<p>hmm... there's this test:</p>
<div class="codehilite"><pre><span></span><span class="w">        </span><span class="n">program</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">            </span><span class="k">trait</span><span class="w"> </span><span class="nb">Iterator</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="k">type</span> <span class="nc">Item</span><span class="p">;</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
<span class="w">            </span><span class="k">struct</span> <span class="nb">Vec</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
<span class="w">            </span><span class="k">struct</span> <span class="kt">u32</span> <span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
<span class="w">            </span><span class="k">impl</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="nb">Iterator</span><span class="w"> </span><span class="k">for</span><span class="w"> </span><span class="nb">Vec</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">                </span><span class="k">type</span> <span class="nc">Item</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="n">T</span><span class="p">;</span><span class="w"></span>
<span class="w">            </span><span class="p">}</span><span class="w"></span>
<span class="w">        </span><span class="p">}</span><span class="w"></span>

<span class="w">        </span><span class="n">goal</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">            </span><span class="n">forall</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">                </span><span class="k">if</span><span class="w"> </span><span class="p">(</span><span class="n">T</span>: <span class="nb">Iterator</span><span class="p">)</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">                    </span><span class="n">exists</span><span class="o">&lt;</span><span class="n">U</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">                        </span><span class="o">&lt;</span><span class="n">T</span><span class="w"> </span><span class="k">as</span><span class="w"> </span><span class="nb">Iterator</span><span class="o">&gt;</span>::<span class="n">Item</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="o">&lt;</span><span class="n">U</span><span class="w"> </span><span class="k">as</span><span class="w"> </span><span class="nb">Iterator</span><span class="o">&gt;</span>::<span class="n">Item</span><span class="w"></span>
<span class="w">                    </span><span class="p">}</span><span class="w"></span>
<span class="w">                </span><span class="p">}</span><span class="w"></span>
<span class="w">            </span><span class="p">}</span><span class="w"></span>
<span class="w">        </span><span class="p">}</span><span class="w"> </span><span class="n">yields</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">            </span><span class="c1">// True for `U = T`, of course, but also true for `U = Vec&lt;T&gt;`.</span>
<span class="w">            </span><span class="s">&quot;Ambiguous&quot;</span><span class="w"></span>
<span class="w">        </span><span class="p">}</span><span class="w"></span>
</pre></div>


<p>I fail to understand how that can be true. With <code>U = Vec&lt;T&gt;</code>, <code>&lt;U as Iterator&gt;::Item = T</code>, and there's no reason why <code>&lt;T as Iterator&gt;::Item = T</code> would hold? Is this test just succeeding because of <a href="https://github.com/rust-lang/chalk/issues/234" target="_blank" title="https://github.com/rust-lang/chalk/issues/234">rust-lang/chalk#234</a>?</p>



<a name="190844428"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190844428" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190844428">(Mar 17 2020 at 13:09)</a>:</h4>
<p>goal 3 of <code>normalize_under_binder</code> seems to be another example that's not actually ambiguous</p>



<a name="190844674"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190844674" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190844674">(Mar 17 2020 at 13:11)</a>:</h4>
<p>also goal 1</p>



<a name="190844850"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190844850" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190844850">(Mar 17 2020 at 13:12)</a>:</h4>
<p>(I've implemented the lower priority for the fallback clause, but haven't implemented the "are the inputs equal" check yet, and am looking for a test that fails because of it to understand better how the check needs to work...)</p>



<a name="190857834"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190857834" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190857834">(Mar 17 2020 at 14:48)</a>:</h4>
<p>I think I've found my example, and am starting to get an idea... I'm thinking to substitute the found solutions into the domain goal we're trying to solve, get the 'inputs' of the substituted domain goal, and check whether they're equal</p>



<a name="190879149"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190879149" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190879149">(Mar 17 2020 at 16:59)</a>:</h4>
<p>hmm, I think you're right that the comment is confused.</p>



<a name="190902137"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190902137" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190902137">(Mar 17 2020 at 19:52)</a>:</h4>
<p>btw awesome <span class="user-mention" data-user-id="129457">@Florian Diebold</span> to hear you are making progress! I'd like to take a look, is it in that same branch?</p>



<a name="190904469"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190904469" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190904469">(Mar 17 2020 at 20:09)</a>:</h4>
<p>Yes, I'm not sure whether I pushed everything</p>



<a name="190960057"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190960057" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190960057">(Mar 18 2020 at 10:14)</a>:</h4>
<p>I did push everything, it's very much WIP and not very nice code in the places where I fixed things though ;)</p>



<a name="190960152"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190960152" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190960152">(Mar 18 2020 at 10:15)</a>:</h4>
<p>Here's another failure:</p>
<div class="codehilite"><pre><span></span>goal { exists &lt; &#39;a &gt; { forall &lt; &#39;b &gt; { exists &lt; &#39;c &gt; { &#39;a = &#39;c, &#39;c = &#39;b } } } }
using solver: Recursive { overflow_depth: 100, caching_enabled: false }
expected:
Unique; for&lt;?U0&gt; { substitution [?0 := &#39;^0, ?1 := &#39;!1_0], lifetime constraints [InEnvironment { environment: Env([]), goal: &#39;^0 == &#39;!1_0 }] }
actual:
Unique; for&lt;?U0&gt; { substitution [?0 := &#39;^0, ?1 := &#39;^0], lifetime constraints [InEnvironment { environment: Env([]), goal: &#39;^0 == &#39;!1_0 }] }
</pre></div>


<p>those are equivalent, right? or is it a requirement that the <code>^0</code> gets substituted there?</p>



<a name="190977262"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/190977262" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#190977262">(Mar 18 2020 at 13:11)</a>:</h4>
<p>I've implemented the 'are the inputs the same' check in a crude way, and also added floundering on too-general goals and goal truncation similar to the SLG solver (also in a crude way <span aria-label="wink" class="emoji emoji-1f609" role="img" title="wink">:wink:</span> ). I'm down to 3 failures, the one above and two that seem to be infinite-looping...</p>



<a name="191029175"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/191029175" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#191029175">(Mar 18 2020 at 19:19)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> ok, the infinite loop actually is caused by the <code>AliasEq</code> logic... it's kind of complicated:</p>
<div class="codehilite"><pre><span></span>WellFormed(str: Sized)
-&gt; Implemented(str: Sized)
   -&gt; FromEnv(str: Sized)
      -&gt; AliasEq(&lt;i32 as Foo&gt;::Item = str)
         -&gt; Normalize(&lt;i32 as Foo&gt;::Item -&gt; str)
            -&gt; Implemented(&lt;i32 as Foo&gt;::Item: Sized)
               -&gt; AliasEq(&lt;i32 as Foo&gt;::Item = ^0) &amp;&amp; FromEnv(^0: Sized)
                  -&gt; Normalize(&lt;i32 as Foo&gt;::Item -&gt; ^0)
                     - Implemented(&lt;i32 as Foo&gt;::Item: Sized) gives cycle error; first attempt: no solution
                  hence ^0 = (Foo::Item)&lt;i32&gt;
                  hence Implemented(&lt;i32 as Foo&gt;::Item: Sized) has solution

               -&gt; AliasEq(&lt;i32 as Foo&gt;::Item = ^0) &amp;&amp; FromEnv(^0: Sized)
                  -&gt; Normalize(&lt;i32 as Foo&gt;::Item -&gt; ^0)
                     - Implemented(&lt;i32 as Foo&gt;::Item: Sized) gives cycle error; second attempt: has solution
                  hence ^0 = str
                  but trying to then prove FromEnv(str: Sized) gives cycle error -&gt; no solution
                  hence Implemented(&lt;i32 as Foo&gt;::Item: Sized) has no solution
</pre></div>


<p>so while trying to prove <code>Implemented(&lt;i32 as Foo&gt;::Item: Sized)</code>, we oscillate between having a solution and having no solution and never exit the loop. The loop for dealing with cycles is based on the assumption that the solution will increase under <a href="https://github.com/flodiebold/chalk/blob/5b3f5b91541706dc13475c0a5bb72e27c6334cb4/chalk-solve/src/recursive/mod.rs#L208-L216" target="_blank" title="https://github.com/flodiebold/chalk/blob/5b3f5b91541706dc13475c0a5bb72e27c6334cb4/chalk-solve/src/recursive/mod.rs#L208-L216">this partial order</a>, but the prioritization logic kind of breaks this by giving a completely different answer.</p>
<p>any idea how to salvage this?</p>



<a name="191044462"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/191044462" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#191044462">(Mar 18 2020 at 21:27)</a>:</h4>
<p><span class="user-mention" data-user-id="129457">@Florian Diebold</span> yeah I had though about this and expected to take prioritization into account</p>



<a name="191044473"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/191044473" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#191044473">(Mar 18 2020 at 21:27)</a>:</h4>
<p>basically to say that we remember the priority</p>



<a name="191044571"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/191044571" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#191044571">(Mar 18 2020 at 21:28)</a>:</h4>
<p>anyway I'll have to look into the code a bit more deeply to say this more precisely</p>



<a name="191044650"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/191044650" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#191044650">(Mar 18 2020 at 21:29)</a>:</h4>
<p>but in short I think that we can treat a higher priority answer as "subsuming" a lower priority answer -- i.e., where you would've used the lower priority one, you should be able to use the higher priority one too equivalently (interstingly, this ought to be true "globally" of Rust programs, but perhaps not "locally" -- i.e., if some associated type is supposed to have a bound <code>type T: Debug</code>, and you supply a value that is not <code>Debug</code></p>



<a name="191044668"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/191044668" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#191044668">(Mar 18 2020 at 21:30)</a>:</h4>
<p>then the placeholder would be considered <code>Debug</code> but the true type would not</p>



<a name="191044733"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/191044733" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#191044733">(Mar 18 2020 at 21:30)</a>:</h4>
<p>there would be an error in the WF checking for the impl of course</p>



<a name="191673028"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/191673028" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#191673028">(Mar 24 2020 at 21:12)</a>:</h4>
<p>to give an update here, I implemented something that keeps track of the priority and lets a high-priority answer just override the low-priority one, which fixes the loop, though the tests still fail because they give different answers than SLG now</p>



<a name="191673105"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/191673105" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#191673105">(Mar 24 2020 at 21:13)</a>:</h4>
<p>I also tried using the recursive solver with rust-analyzer, but it seems there's another endless loop which I haven't investigated yet...</p>



<a name="191753158"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/191753158" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#191753158">(Mar 25 2020 at 14:30)</a>:</h4>
<blockquote>
<p>the tests still fail because they give different answers than SLG now</p>
</blockquote>
<p>and I'm not sure whether it's a <em>requirement</em> that we give the same answer as SLG in IMO nonsensical cases like the one in that test, which is basically</p>
<div class="codehilite"><pre><span></span><span class="k">trait</span><span class="w"> </span><span class="n">Foo</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="k">type</span> <span class="nc">Item</span>: <span class="nb">Sized</span> <span class="nc">where</span><span class="w"> </span><span class="n">Self</span>::<span class="n">Item</span>: <span class="nb">Sized</span><span class="p">;</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
<span class="k">impl</span><span class="w"> </span><span class="n">Foo</span><span class="w"> </span><span class="k">for</span><span class="w"> </span><span class="kt">i32</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="k">type</span> <span class="nc">Item</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="kt">str</span><span class="p">;</span><span class="w"> </span><span class="c1">// not Sized</span>
<span class="p">}</span><span class="w"></span>
</pre></div>


<p>I mean, at least that doesn't make sense to me...</p>



<a name="192055413"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/192055413" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#192055413">(Mar 27 2020 at 17:51)</a>:</h4>
<blockquote>
<p>I also tried using the recursive solver with rust-analyzer, but it seems there's another endless loop which I haven't investigated yet...</p>
</blockquote>
<p>Ok, I fixed that, and RA works with the recursive solver now. It fixes about 500 unknown types in the RA codebase, which is a good number, though less than I'd have hoped. And it's a lot slower, making RA take about double the time for type inference</p>



<a name="192055544"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/192055544" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#192055544">(Mar 27 2020 at 17:52)</a>:</h4>
<p>(probably there's some low-hanging fruit somewhere though, and there's a lot of potential for better caching)</p>



<a name="192371873"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/192371873" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#192371873">(Mar 31 2020 at 10:43)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> what do you think about moving the floundering-on-too-general-goals logic to the program clauses code? I think it makes sense to share it between the solvers, and also I needed to add floundering for too general <code>Normalize</code> goals (since the program clauses logic for them also will try to enumerate all impls). and it just feels like the program clauses logic actually knows better what goals are too general</p>



<a name="192381706"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/192381706" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#192381706">(Mar 31 2020 at 12:30)</a>:</h4>
<p><span class="user-mention" data-user-id="129457">@Florian Diebold</span> I'm not sure which logic you're referring to exactly -- the logic that prevents things from being enumerated currently lives in the chalk-solve code, which I would expect to be shared by the recursive solver</p>



<a name="192382487"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/192382487" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#192382487">(Mar 31 2020 at 12:37)</a>:</h4>
<p>it lives in <a href="https://github.com/rust-lang/chalk/blob/1ac0d00e61b427964c2b9b10e21bd8cd183e5932/chalk-solve/src/solve/slg.rs#L188-L212" title="https://github.com/rust-lang/chalk/blob/1ac0d00e61b427964c2b9b10e21bd8cd183e5932/chalk-solve/src/solve/slg.rs#L188-L212"><code>chalk_solve::solve::slg</code></a>, so I have to move it <em>somewhere</em> to share it.</p>
<p>but also, for the <code>Normalize</code> floundering logic, I need it to <em>not</em> return ambiguous if we have a goal like <code>Normalize(&lt;?0 as SomeTrait&gt;::Assoc -&gt; SomeTrait::Assoc&lt;SomeType&gt;)</code>, because we <em>know</em> this particular goal won't have a solution, and if we return ambiguous there, it breaks things (because then the <code>AliasEq(&lt;?0 as SomeTrait&gt;::Assoc = SomeTrait::Assoc&lt;SomeType&gt;)</code> will also be ambiguous). So the logic becomes more intertwined with the program clauses logic there</p>



<a name="192382946"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/192382946" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#192382946">(Mar 31 2020 at 12:41)</a>:</h4>
<p>I see. Yeah I have no problem moving that logic to <code>program_clauses_for_goal</code></p>



<a name="192382957"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/192382957" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#192382957">(Mar 31 2020 at 12:41)</a>:</h4>
<p>In fact I sort of thought that's where it lived already</p>



<a name="192382994"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/192382994" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#192382994">(Mar 31 2020 at 12:41)</a>:</h4>
<p>I'm not sure I understand the Normalize case yet</p>



<a name="192383137"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/192383137" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#192383137">(Mar 31 2020 at 12:42)</a>:</h4>
<p>(How do we know that won't have a solution, for one thing?)</p>



<a name="192383177"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/192383177" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#192383177">(Mar 31 2020 at 12:43)</a>:</h4>
<p>Do we return ambiguous today? I thought that the flounder logic applied only to <code>Implemented</code> goals...?</p>



<a name="192384606"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/192384606" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#192384606">(Mar 31 2020 at 12:54)</a>:</h4>
<p><span class="user-mention silent" data-user-id="116009">nikomatsakis</span> <a href="#narrow/stream/144729-wg-traits/topic/recursive.20solver/near/192383177" title="#narrow/stream/144729-wg-traits/topic/recursive.20solver/near/192383177">said</a>:</p>
<blockquote>
<p>Do we return ambiguous today? I thought that the flounder logic applied only to <code>Implemented</code> goals...?</p>
</blockquote>
<p>We don't, but when testing the recursive solver with RA, I ran into it trying to enumerate all impls for <code>Iterator</code> to solve something like <code>Normalize(&lt;?0 as Iterator&gt;::Item -&gt; Something)</code>. I <em>think</em> we should apply the same logic as for <code>Implemented</code> goals there.</p>
<blockquote>
<p>(How do we know that won't have a solution, for one thing?)</p>
</blockquote>
<p>hmm maybe I have a misunderstanding here, but I think nothing can ever <code>Normalize</code> to an assoc type placeholder since the right-hand side of <code>Normalize</code> is always some type written by a user, and you can't write assoc type placeholders. (When we have something like <code>type Item = &lt;T as OtherTrait&gt;::OtherType</code>, I think that would still be a <code>TyData::Alias</code>?)</p>



<a name="192388717"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/192388717" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#192388717">(Mar 31 2020 at 13:26)</a>:</h4>
<p>That's not true, it could normalize to an associated type placeholder. For example, you might have</p>
<div class="codehilite"><pre><span></span><span class="k">impl</span><span class="o">&lt;</span><span class="n">A</span>: <span class="nb">Iterator</span><span class="o">&gt;</span><span class="w"> </span><span class="n">Foo</span><span class="o">&lt;</span><span class="n">A</span><span class="o">&gt;</span><span class="w"> </span><span class="k">for</span><span class="w"> </span><span class="kt">u32</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="k">type</span> <span class="nc">Bar</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="n">A</span>::<span class="n">Item</span><span class="p">;</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>

<span class="k">fn</span> <span class="nf">baz</span><span class="o">&lt;</span><span class="n">T</span>: <span class="nb">Iterator</span><span class="o">&gt;</span><span class="p">()</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="p">...</span><span class="w"> </span><span class="o">&lt;</span><span class="kt">u32</span><span class="w"> </span><span class="k">as</span><span class="w"> </span><span class="n">Foo</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;&gt;</span>::<span class="n">Bar</span><span class="w"> </span><span class="p">...</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
</pre></div>



<a name="192388954"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/192388954" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#192388954">(Mar 31 2020 at 13:29)</a>:</h4>
<p><span class="user-mention silent" data-user-id="129457">Florian Diebold</span> <a href="#narrow/stream/144729-wg-traits/topic/recursive.20solver/near/192384606" title="#narrow/stream/144729-wg-traits/topic/recursive.20solver/near/192384606">said</a>:</p>
<blockquote>
<p>We don't, but when testing the recursive solver with RA, I ran into it trying to enumerate all impls for <code>Iterator</code> to solve something like <code>Normalize(&lt;?0 as Iterator&gt;::Item -&gt; Something)</code>. I <em>think</em> we should apply the same logic as for <code>Implemented</code> goals there.</p>
</blockquote>
<p>so this is an interesting question too. The compiler never uses the <code>-&gt; Something</code> part to figure out the result -- it looks purely at the inputs. And, I suspect, it probably has a rule  about unknown self types. At minimum, that would yield an ambiguous result when looking for trait impls, which would lead to overall ambiguity I think.</p>
<p>I have been debating with myself over time whether we would <em>want</em> to be able to (e.g.) deduce what <code>?0</code> is based on the <em>target type</em> of the normalization. There are some scenarios where it would be uesful. We have some special case hacks in the compiler, for example, to handle things like <code>let x: u32 = 22 + 44</code>, which requires us to deduce that 22 and 44 must be <code>u32</code> because the <em>output type</em> is <code>u32</code>.</p>



<a name="192388976"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/192388976" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#192388976">(Mar 31 2020 at 13:29)</a>:</h4>
<p>But I'd be happy to match rustc's behavior for now.</p>



<a name="192391259"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/192391259" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#192391259">(Mar 31 2020 at 13:45)</a>:</h4>
<p><span class="user-mention" data-user-id="129457">@Florian Diebold</span> so i'm reading over the recursive solver branch again</p>



<a name="192391273"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/192391273" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#192391273">(Mar 31 2020 at 13:45)</a>:</h4>
<p>it looks reasonably close to what I envisioned</p>



<a name="192391281"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/192391281" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#192391281">(Mar 31 2020 at 13:45)</a>:</h4>
<p>which tests are you currently looking at?</p>



<a name="192391495"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/192391495" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#192391495">(Mar 31 2020 at 13:47)</a>:</h4>
<p>I see a few obvious refactorings I had in mind, though not critical to the problems we were discussing</p>
<ul>
<li>refactoring the <code>program_clauses_for_goal</code> and <code>program_clauses_for_env</code> logic a bit. </li>
<li>separating out the "global cache" from the "per-thread solver", to allow for better multi-thread integration in rust-analyzer etc</li>
</ul>



<a name="192391733"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/192391733" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#192391733">(Mar 31 2020 at 13:49)</a>:</h4>
<ul>
<li>remove the overflow checking and replace with truncation logic instead</li>
</ul>



<a name="192391782"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/192391782" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#192391782">(Mar 31 2020 at 13:49)</a>:</h4>
<ul>
<li>convert tests to run with <em>both</em> solvers, like they used to?</li>
</ul>



<a name="192391875"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/192391875" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#192391875">(Mar 31 2020 at 13:50)</a>:</h4>
<p>( I was wondering in particular if it'd be good to land the solver in tree so we can collaborate a bit more on it -- or maybe it's good living where it is, or even could land on a branch in rust-lang?)</p>



<a name="192392059"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/192392059" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#192392059">(Mar 31 2020 at 13:51)</a>:</h4>
<p>1 and 4 are already on my list <span aria-label="slight smile" class="emoji emoji-1f642" role="img" title="slight smile">:slight_smile:</span> as to 3... I did add truncation (I don't know whether in the right place), so I don't actually know whether the overflow check is still necessary</p>



<a name="192395007"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/192395007" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#192395007">(Mar 31 2020 at 14:13)</a>:</h4>
<p>so, the problem why I wanted to cut <code>Normalize(&lt;?0 as SomeTrait&gt;::Assoc -&gt; SomeTrait::Assoc&lt;SomeType&gt;)</code> short was that <code>AliasEq(&lt;?0 as SomeTrait&gt;::Assoc = SomeTrait::Assoc&lt;SomeType&gt;)</code> shows up as a goal that I think we need to be able to solve. The concrete case was the <code>lowering::assoc_tys</code> test, where it'll need to solve <code>Implemented((Iterator::Item)&lt;!1_0&gt;: Foo)</code> in <code>Env([for&lt;&gt; FromEnv(!1_0: Iterator), FromEnv(&lt;!1_0 as Iterator&gt;::Item)])</code> at some point, and that requires <code>AliasEq(&lt;^0.0 as Iterator&gt;::Item = (Iterator::Item)&lt;!1_0&gt;)</code> since it unifies it with <code>Implemented(&lt;?0 as Iterator&gt;::Item: Foo)</code>. Solving <code>AliasEq(&lt;^0.0 as Iterator&gt;::Item = (Iterator::Item)&lt;!1_0&gt;)</code> seems like it should be easy, but if the <code>Normalize</code> rule returns ambiguous we have no way of making progress</p>



<a name="192398625"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/192398625" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#192398625">(Mar 31 2020 at 14:41)</a>:</h4>
<p>I thought it'd make sense to land the solver once the tests work with both solvers</p>



<a name="192422083"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/192422083" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#192422083">(Mar 31 2020 at 17:27)</a>:</h4>
<p>Regarding <code>test::unify::unify_quantified_lifetimes</code>, I think the new output is equivalent, i'm not 100% sure why it turns out different but it seems 'ok'</p>



<a name="192952934"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/192952934" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#192952934">(Apr 05 2020 at 10:34)</a>:</h4>
<p>I'm now running all tests for both solvers by default (except for the lowering tests, which hides at least one test failure currently)</p>



<a name="192952952"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/192952952" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#192952952">(Apr 05 2020 at 10:35)</a>:</h4>
<p>also, I refactored the env clauses handling a bit; <code>program_clauses_for_env</code> didn't actually add the env clauses themselves, which seemed weird, so now it does that and I removed the corresponding code from both solvers</p>



<a name="192952964"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/192952964" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#192952964">(Apr 05 2020 at 10:35)</a>:</h4>
<p>I've removed the <code>Normalize</code> floundering for the moment, but I think we'll need some solution there</p>



<a name="192953247"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/192953247" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#192953247">(Apr 05 2020 at 10:42)</a>:</h4>
<p>(regarding the env clause handling, I've also removed the code that favored env solutions over program clause solutions; it didn't break any tests at the moment)</p>



<a name="192957642"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/192957642" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#192957642">(Apr 05 2020 at 12:41)</a>:</h4>
<p>I made a <a href="https://github.com/rust-lang/chalk/pull/372" title="https://github.com/rust-lang/chalk/pull/372">pull request</a>, so you should even be able to push to the branch now</p>



<a name="193097985"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193097985" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193097985">(Apr 06 2020 at 20:34)</a>:</h4>
<p><span class="user-mention silent" data-user-id="129457">Florian Diebold</span> <a href="#narrow/stream/144729-wg-traits/topic/recursive.20solver/near/192953247" title="#narrow/stream/144729-wg-traits/topic/recursive.20solver/near/192953247">said</a>:</p>
<blockquote>
<p>(regarding the env clause handling, I've also removed the code that favored env solutions over program clause solutions; it didn't break any tests at the moment)</p>
</blockquote>
<p>yeah that's ok we can add that back later</p>



<a name="193874322"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193874322" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193874322">(Apr 14 2020 at 09:59)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> I'd like to start considering merging the branch, rebasing it over all the refactorings happening at the moment is a lot of work <span aria-label="sweat smile" class="emoji emoji-1f605" role="img" title="sweat smile">:sweat_smile:</span> </p>
<p>It's working well with RA now, though I added back the floundering on Normalize because it otherwise wasn't usable</p>



<a name="193875509"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193875509" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193875509">(Apr 14 2020 at 10:10)</a>:</h4>
<p><span class="user-mention" data-user-id="129457">@Florian Diebold</span> Yes! I was hoping to review this morning. Sorry for the delay. Reading <span class="user-mention" data-user-id="125131">@detrumi</span>'s impl Trait PR right now, since I neglected that one, too.</p>



<a name="193875517"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193875517" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193875517">(Apr 14 2020 at 10:10)</a>:</h4>
<p>Suddenly there's a lot to review!</p>



<a name="193875571"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193875571" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193875571">(Apr 14 2020 at 10:11)</a>:</h4>
<p>let me check whether I've pushed the current version, though</p>



<a name="193875693"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193875693" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193875693">(Apr 14 2020 at 10:12)</a>:</h4>
<p>Side note that I realized the recursive solver interacts (negatively, in a sense) with some of my plans around solving higher-ranked region constraints.</p>



<a name="193875706"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193875706" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193875706">(Apr 14 2020 at 10:12)</a>:</h4>
<p>But I'll worry about that later. :)</p>



<a name="193875808"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193875808" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193875808">(Apr 14 2020 at 10:13)</a>:</h4>
<p>In particular, I wanted to have use the SLG solver's ability to enumerate all possible solutions to figure out things like "which regions might outlive <code>'a</code> given something like <code>forall&lt;'a&gt; { if ('b: 'a) { _: 'a } }</code></p>



<a name="193875814"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193875814" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193875814">(Apr 14 2020 at 10:13)</a>:</h4>
<p>but there were other problems to consider with that approach anyway</p>



<a name="193875888"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193875888" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193875888">(Apr 14 2020 at 10:14)</a>:</h4>
<p>Also I know I have to ping you about salsa integration, not sure if you did anything in that direction at all</p>



<a name="193876569"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193876569" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193876569">(Apr 14 2020 at 10:21)</a>:</h4>
<p>I also don't know how we'll handle integer/float variables with the recursive solver, with SLG we could just have a trait <code>?0: Integer</code> in the environment, but the recursive solver might need special knowledge of them after all</p>



<a name="193877072"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193877072" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193877072">(Apr 14 2020 at 10:26)</a>:</h4>
<p>Yeah, I'm kind of expecting I'll have to give way and just add them</p>



<a name="193877094"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193877094" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193877094">(Apr 14 2020 at 10:26)</a>:</h4>
<p>tbh I was sort of expecting that before, for efficiency reasons</p>



<a name="193879506"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193879506" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193879506">(Apr 14 2020 at 10:52)</a>:</h4>
<p><span class="user-mention" data-user-id="129457">@Florian Diebold</span> did a first pass, I didn't get to the solver itself yet, just the code around it -- the main thing is that I'd like to avoid commenting out tests and instead document the existing behavior for both sovlers (and add FIXME if needed)</p>



<a name="193879528"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193879528" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193879528">(Apr 14 2020 at 10:52)</a>:</h4>
<p>really nice work btw <span aria-label="sparkling heart" class="emoji emoji-1f496" role="img" title="sparkling heart">:sparkling_heart:</span></p>



<a name="193961161"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193961161" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193961161">(Apr 14 2020 at 21:49)</a>:</h4>
<p>One thing that's a bit surprising to me</p>



<a name="193961169"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193961169" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193961169">(Apr 14 2020 at 21:50)</a>:</h4>
<p>is that this solver is able to handle all the coinduction tests</p>



<a name="193961645"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193961645" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193961645">(Apr 14 2020 at 21:55)</a>:</h4>
<p><em>ah</em> I see</p>



<a name="193961661"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193961661" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193961661">(Apr 14 2020 at 21:55)</a>:</h4>
<p>those tests are (for some reason) written like </p>
<div class="codehilite"><pre><span></span><span class="w">        </span><span class="n">goal</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">            </span><span class="n">forall</span><span class="o">&lt;</span><span class="n">X</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="n">X</span>: <span class="nc">C1orC2</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
<span class="w">        </span><span class="p">}</span><span class="w"> </span><span class="n">yields_all</span><span class="p">[</span><span class="n">SolverChoice</span>::<span class="n">slg</span><span class="p">(</span><span class="mi">3</span><span class="p">,</span><span class="w"> </span><span class="nb">None</span><span class="p">)]</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">        </span><span class="p">}</span><span class="w"></span>
</pre></div>



<a name="193961677"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193961677" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193961677">(Apr 14 2020 at 21:55)</a>:</h4>
<p><span class="user-mention" data-user-id="232957">@Jack Huey</span> do you remember why you did that?</p>



<a name="193961712"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193961712" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193961712">(Apr 14 2020 at 21:55)</a>:</h4>
<p>(as opposed to <code>yields</code>)</p>



<a name="193961761"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193961761" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193961761">(Apr 14 2020 at 21:56)</a>:</h4>
<p>uh</p>



<a name="193961771"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193961771" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193961771">(Apr 14 2020 at 21:56)</a>:</h4>
<p>hmm</p>



<a name="193961795"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193961795" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193961795">(Apr 14 2020 at 21:56)</a>:</h4>
<p>I wonder if that had to do with</p>



<a name="193961801"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193961801" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193961801">(Apr 14 2020 at 21:56)</a>:</h4>
<p>how the slg testes used to have different macros</p>



<a name="193961803"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193961803" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193961803">(Apr 14 2020 at 21:56)</a>:</h4>
<p>tha you unified at some point?</p>



<a name="193961814"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193961814" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193961814">(Apr 14 2020 at 21:56)</a>:</h4>
<p>I think it was because specifically wanted to test that no answers were given</p>



<a name="193961822"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193961822" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193961822">(Apr 14 2020 at 21:56)</a>:</h4>
<p>it seems like</p>



<a name="193961824"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193961824" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193961824">(Apr 14 2020 at 21:56)</a>:</h4>
<p>but yeah, it might have also been because of the macros</p>



<a name="193961826"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193961826" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193961826">(Apr 14 2020 at 21:56)</a>:</h4>
<div class="codehilite"><pre><span></span><span class="w">        </span><span class="n">goal</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">            </span><span class="n">forall</span><span class="o">&lt;</span><span class="n">X</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="n">X</span>: <span class="nc">C1orC2</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
<span class="w">        </span><span class="p">}</span><span class="w"> </span><span class="n">yields</span><span class="p">[</span><span class="n">SolverChoice</span>::<span class="n">slg</span><span class="p">(</span><span class="mi">3</span><span class="p">,</span><span class="w"> </span><span class="nb">None</span><span class="p">)]</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">            </span><span class="s">&quot;No possible solution&quot;</span><span class="w"></span>
<span class="w">        </span><span class="p">}</span><span class="w"></span>
</pre></div>



<a name="193961829"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193961829" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193961829">(Apr 14 2020 at 21:57)</a>:</h4>
<p>is more or less equivalent?</p>



<a name="193961840"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193961840" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193961840">(Apr 14 2020 at 21:57)</a>:</h4>
<p>the only reason I mention it is that the recursive solver doesn't support <code>yields_all</code></p>



<a name="193961850"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193961850" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193961850">(Apr 14 2020 at 21:57)</a>:</h4>
<p>and it'd be nice for the tests to be "as analogous as possible"</p>



<a name="193961851"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193961851" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193961851">(Apr 14 2020 at 21:57)</a>:</h4>
<p>but doesn't matter that much</p>



<a name="193961861"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193961861" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193961861">(Apr 14 2020 at 21:57)</a>:</h4>
<p>in any case the recursive solver does indeed fail  here</p>



<a name="193961871"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193961871" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193961871">(Apr 14 2020 at 21:57)</a>:</h4>
<p>as expected</p>



<a name="193961873"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193961873" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193961873">(Apr 14 2020 at 21:57)</a>:</h4>
<p>if you mean <code>yields</code> there?</p>



<a name="193961874"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193961874" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193961874">(Apr 14 2020 at 21:57)</a>:</h4>
<p>which is good because otherwise I was quite confused</p>



<a name="193961882"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193961882" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193961882">(Apr 14 2020 at 21:57)</a>:</h4>
<div class="codehilite"><pre><span></span><span class="w">        </span><span class="n">goal</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">            </span><span class="n">forall</span><span class="o">&lt;</span><span class="n">X</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="n">X</span>: <span class="nc">C1orC2</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
<span class="w">        </span><span class="p">}</span><span class="w"> </span><span class="n">yields</span><span class="p">[</span><span class="n">SolverChoice</span>::<span class="n">recursive</span><span class="p">()]</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">            </span><span class="s">&quot;No possible solution&quot;</span><span class="w"></span>
<span class="w">        </span><span class="p">}</span><span class="w"></span>
</pre></div>



<a name="193961888"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193961888" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193961888">(Apr 14 2020 at 21:58)</a>:</h4>
<p>that's the test for the recursive solver, I mean</p>



<a name="193961924"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193961924" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193961924">(Apr 14 2020 at 21:58)</a>:</h4>
<p>ah</p>



<a name="193961945"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193961945" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193961945">(Apr 14 2020 at 21:58)</a>:</h4>
<p>yeah, I think that's equivalent</p>



<a name="193962023"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193962023" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193962023">(Apr 14 2020 at 21:59)</a>:</h4>
<p>the other question is why <code>slg(3, None)</code> in particular</p>



<a name="193962037"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193962037" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193962037">(Apr 14 2020 at 21:59)</a>:</h4>
<p>(vs the default)</p>



<a name="193962057"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193962057" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193962057">(Apr 14 2020 at 21:59)</a>:</h4>
<p>I'm not sure</p>



<a name="193962207"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193962207" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193962207">(Apr 14 2020 at 22:01)</a>:</h4>
<p>I don't <em>think</em> that's important</p>



<a name="193962277"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193962277" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193962277">(Apr 14 2020 at 22:02)</a>:</h4>
<p>if you change it to 10, does the test still pass</p>



<a name="193962853"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193962853" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193962853">(Apr 14 2020 at 22:07)</a>:</h4>
<p>yes the tests all still pass</p>



<a name="193962863"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193962863" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193962863">(Apr 14 2020 at 22:07)</a>:</h4>
<p>I changed them</p>



<a name="193962885"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193962885" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193962885">(Apr 14 2020 at 22:07)</a>:</h4>
<p>because in some cases that lets me write <code>goal { } yields { }</code> to test "all solvers"</p>



<a name="193962977"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193962977" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193962977">(Apr 14 2020 at 22:08)</a>:</h4>
<p><span class="user-mention" data-user-id="129457">@Florian Diebold</span> I pushed a commit to your branch that ensures all tests run for the recursive solver--</p>



<a name="193963078"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193963078" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193963078">(Apr 14 2020 at 22:10)</a>:</h4>
<p>two commits, now</p>



<a name="193963128"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193963128" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193963128">(Apr 14 2020 at 22:10)</a>:</h4>
<p>but with that, I think I am satisfied to land, though we should definitely file some follow-up issues</p>



<a name="193963133"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193963133" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193963133">(Apr 14 2020 at 22:10)</a>:</h4>
<p>notably around coinduction</p>



<a name="193963153"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193963153" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193963153">(Apr 14 2020 at 22:10)</a>:</h4>
<p>I guess I should read over the priority code carefully</p>



<a name="193963211"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193963211" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193963211">(Apr 14 2020 at 22:11)</a>:</h4>
<p>ah, ok, so I think this is incomplete</p>



<a name="193963212"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193963212" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193963212">(Apr 14 2020 at 22:11)</a>:</h4>
<p>I'd like to try and write a test that exercises that</p>



<a name="193964076"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193964076" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193964076">(Apr 14 2020 at 22:20)</a>:</h4>
<p>ok well I can't think of a test right now :P</p>



<a name="193964086"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193964086" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193964086">(Apr 14 2020 at 22:20)</a>:</h4>
<p>sorry, to elaborate</p>



<a name="193964097"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193964097" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193964097">(Apr 14 2020 at 22:20)</a>:</h4>
<p>the current code <em>always</em> prefers a higher-priority solution</p>



<a name="193964105"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193964105" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193964105">(Apr 14 2020 at 22:20)</a>:</h4>
<p>even if the higher-priority solution is not 'fully general'</p>



<a name="193964110"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193964110" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193964110">(Apr 14 2020 at 22:20)</a>:</h4>
<p>at least if I'm reading it correctly</p>



<a name="193964151"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193964151" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193964151">(Apr 14 2020 at 22:21)</a>:</h4>
<p>so if you have something like <code>&lt;T as Trait&lt;?X&gt;&gt;::Foo</code>, and an impl that gives <code>T: Trait&lt;S1&gt;</code>, it would say that <code>?X = S1</code></p>



<a name="193964169"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193964169" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193964169">(Apr 14 2020 at 22:21)</a>:</h4>
<p>which..is not <em>wrong</em>, i.e., in terms of the impls we see, it's correct, and rustc often makes such leaps (for better and worse)</p>



<a name="193964246"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193964246" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193964246">(Apr 14 2020 at 22:22)</a>:</h4>
<p>but at the same time there <em>is</em> another solution available to us, the placeholder, that doesn't require that <code>?X = S1</code></p>



<a name="193964275"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193964275" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193964275">(Apr 14 2020 at 22:22)</a>:</h4>
<p>so in some sense the answer is strange</p>



<a name="193964291"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193964291" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193964291">(Apr 14 2020 at 22:22)</a>:</h4>
<p>but I can't come up with a test that will compile with the placeholder but not without it right now</p>



<a name="193964310"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193964310" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193964310">(Apr 14 2020 at 22:23)</a>:</h4>
<p>I wonder if it's even needed</p>



<a name="193964386"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193964386" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193964386">(Apr 14 2020 at 22:23)</a>:</h4>
<p>I was thinking maybe something like</p>



<a name="193964529"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193964529" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193964529">(Apr 14 2020 at 22:25)</a>:</h4>
<div class="codehilite"><pre><span></span><span class="k">trait</span><span class="w"> </span><span class="n">Foo</span><span class="o">&lt;</span><span class="n">A</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="k">type</span> <span class="nc">Bar</span>: <span class="nc">Debug</span><span class="p">;</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>

<span class="k">impl</span><span class="w"> </span><span class="n">Foo</span><span class="o">&lt;</span><span class="n">S2</span><span class="o">&gt;</span><span class="w"> </span><span class="k">for</span><span class="w"> </span><span class="n">S1</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="k">type</span> <span class="nc">Bar</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="n">S3</span><span class="p">;</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
</pre></div>


<p>and then </p>
<div class="codehilite"><pre><span></span>exists&lt;T, U&gt; {
    S1: Foo&lt;T, Bar = U&gt;,
    U: Debug, // true with the placeholder (or with S3)
    T = S4, // this would error because we forced T to be S2
}
</pre></div>


<p>but of course that won't compile because we don't know that <code>S1: Foo&lt;S4, Bar = U&gt;</code> is true. And if we <em>did</em> know it were true, we'd get an ambiguity and wouldn't have normalized successfully.</p>



<a name="193964620"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193964620" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193964620">(Apr 14 2020 at 22:26)</a>:</h4>
<p>(In particular, it <em>is</em> true that <em>another crate</em> could define <code>Foo&lt;S4&gt; for S1</code> for some <code>S4</code>, but of course we can't see that definition.)</p>



<a name="193965128"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193965128" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193965128">(Apr 14 2020 at 22:31)</a>:</h4>
<p>oh huh</p>



<a name="193965136"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193965136" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193965136">(Apr 14 2020 at 22:31)</a>:</h4>
<p>I found some other weird results...</p>



<a name="193965190"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193965190" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193965190">(Apr 14 2020 at 22:32)</a>:</h4>
<p><del>that do seem like a bug, but for... both the slg and the recursive solver</del></p>



<a name="193965854"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193965854" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193965854">(Apr 14 2020 at 22:39)</a>:</h4>
<p>ok, well, hmm. I guess I'm inclined to land the recursive solver, but I think we should open a follow-up issue to dig a bit more here</p>



<a name="193965896"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193965896" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193965896">(Apr 14 2020 at 22:40)</a>:</h4>
<p>unfortunately I have to run</p>



<a name="193965914"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193965914" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193965914">(Apr 14 2020 at 22:40)</a>:</h4>
<p>I started playing some tests and got some surprising results</p>



<a name="193965919"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/193965919" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#193965919">(Apr 14 2020 at 22:40)</a>:</h4>
<p>that I don't fully understand yet</p>



<a name="194005608"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/194005608" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#194005608">(Apr 15 2020 at 09:39)</a>:</h4>
<p><span class="user-mention silent" data-user-id="116009">nikomatsakis</span> <a href="#narrow/stream/144729-wg-traits/topic/recursive.20solver/near/193963211" title="#narrow/stream/144729-wg-traits/topic/recursive.20solver/near/193963211">said</a>:</p>
<blockquote>
<p>ah, ok, so I think this is incomplete</p>
</blockquote>
<p>this is just wrong, which explains some of my confusion last night. I hadn't found the <code>combine_with_priorities</code> function.</p>



<a name="194006304"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/194006304" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#194006304">(Apr 15 2020 at 09:45)</a>:</h4>
<p>OK, I pushed some updated tests, and I think everything is behaving as expected. Nice job, <span class="user-mention" data-user-id="129457">@Florian Diebold</span>! I left a few comments on the PR, but I think they're all things I'm comfortable addressing in follow up issues.</p>



<a name="194006402"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/194006402" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#194006402">(Apr 15 2020 at 09:46)</a>:</h4>
<p>Oh, well, I'd like to figure out <a href="https://github.com/rust-lang/chalk/pull/372#discussion_r408711359" title="https://github.com/rust-lang/chalk/pull/372#discussion_r408711359">this question</a></p>



<a name="194006472"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/194006472" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#194006472">(Apr 15 2020 at 09:47)</a>:</h4>
<p>yeah I guess we can just use <code>combine_with_priorities</code> there, I wasn't sure about <em>combining</em> solutions from previous iterations</p>



<a name="194006575"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/194006575" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#194006575">(Apr 15 2020 at 09:48)</a>:</h4>
<p>and also, I didn't have a test that produces a problem because of that <span aria-label="grimacing" class="emoji emoji-1f62c" role="img" title="grimacing">:grimacing:</span></p>



<a name="194007402"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/194007402" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#194007402">(Apr 15 2020 at 09:56)</a>:</h4>
<p>Yeah, I was having trouble making a test for that, but now I think I understand a bit better</p>



<a name="194007415"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/194007415" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#194007415">(Apr 15 2020 at 09:57)</a>:</h4>
<p>so I can think about it and maybe grab one</p>



<a name="194007420"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/194007420" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#194007420">(Apr 15 2020 at 09:57)</a>:</h4>
<p>i.e,. I understand where it comes up</p>



<a name="194007452"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/194007452" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#194007452">(Apr 15 2020 at 09:57)</a>:</h4>
<p>it should be ok to combine solutions from previous iterations -- it's actually no different than combining solutions from different program clauses</p>



<a name="194007478"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/194007478" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#194007478">(Apr 15 2020 at 09:57)</a>:</h4>
<p>basically in each case the new solution represents "some possible answer"</p>



<a name="194205431"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/194205431" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#194205431">(Apr 15 2020 at 18:09)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> I've implemented that (though it was more complicated than it seemed at the outset, you can see in the last commit). I've also rebased, and had to change the truncation to flounder like SLG now does. That actually fixed the result for that <code>cycle::overflow</code> test that surprised you</p>



<a name="194226716"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/194226716" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#194226716">(Apr 15 2020 at 20:59)</a>:</h4>
<p>ah interesting</p>



<a name="194226733"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/194226733" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#194226733">(Apr 15 2020 at 20:59)</a>:</h4>
<p>great, then perhaps we'll land this thing wth some follow-up issues</p>



<a name="194659332"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/194659332" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#194659332">(Apr 20 2020 at 10:55)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> <a href="https://github.com/rust-lang/chalk/issues/404" title="https://github.com/rust-lang/chalk/issues/404">rust-lang/chalk#404</a> should be a very fast review and improves performance a lot <span aria-label="grimacing" class="emoji emoji-1f62c" role="img" title="grimacing">:grimacing:</span></p>



<a name="194659454"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/194659454" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#194659454">(Apr 20 2020 at 10:56)</a>:</h4>
<p>You might also want to look at <a href="https://github.com/rust-lang/chalk/issues/403" title="https://github.com/rust-lang/chalk/issues/403">rust-lang/chalk#403</a>, though Jack already merged that one</p>



<a name="194682806"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/194682806" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#194682806">(Apr 20 2020 at 14:31)</a>:</h4>
<p><span class="user-mention silent" data-user-id="129457">Florian Diebold</span> <a href="#narrow/stream/144729-wg-traits/topic/recursive.20solver/near/194659332" title="#narrow/stream/144729-wg-traits/topic/recursive.20solver/near/194659332">said</a>:</p>
<blockquote>
<p><span class="user-mention silent" data-user-id="116009">nikomatsakis</span> <a href="https://github.com/rust-lang/chalk/issues/404" title="https://github.com/rust-lang/chalk/issues/404">rust-lang/chalk#404</a> should be a very fast review and improves performance a lot <span aria-label="grimacing" class="emoji emoji-1f62c" role="img" title="grimacing">:grimacing:</span></p>
</blockquote>
<p>reviewed and merged, <span class="user-mention" data-user-id="129457">@Florian Diebold</span></p>



<a name="194682833"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/194682833" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#194682833">(Apr 20 2020 at 14:31)</a>:</h4>
<p>thanks</p>



<a name="194682872"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/194682872" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#194682872">(Apr 20 2020 at 14:31)</a>:</h4>
<p><span class="user-mention silent" data-user-id="129457">Florian Diebold</span> <a href="#narrow/stream/144729-wg-traits/topic/recursive.20solver/near/194659454" title="#narrow/stream/144729-wg-traits/topic/recursive.20solver/near/194659454">said</a>:</p>
<blockquote>
<p>You might also want to look at <a href="https://github.com/rust-lang/chalk/issues/403" title="https://github.com/rust-lang/chalk/issues/403">rust-lang/chalk#403</a>, though Jack already merged that one</p>
</blockquote>
<p>ah, yeah, I saw that and had that queued for review, though I'm happy that <span class="user-mention" data-user-id="232957">@Jack Huey</span> merged it</p>



<a name="194682948"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/194682948" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#194682948">(Apr 20 2020 at 14:32)</a>:</h4>
<p>I'd like to make the whole "give me the clauses for this goal" thing into a cacheable query</p>



<a name="194682981"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/194682981" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#194682981">(Apr 20 2020 at 14:32)</a>:</h4>
<p>I've been wanting to revisit the <code>RustIrDatabase</code> trait to make that work, I suppose it might be as simple as</p>



<a name="194683008"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/194683008" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#194683008">(Apr 20 2020 at 14:32)</a>:</h4>
<p>having a callback</p>



<a name="194683049"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/194683049" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#194683049">(Apr 20 2020 at 14:32)</a>:</h4>
<p>which actually suggests that maybe you were right to make the input be the <code>Canonical</code> gola in environment</p>



<a name="194683073"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/194683073" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#194683073">(Apr 20 2020 at 14:32)</a>:</h4>
<p>and maybe we should even refactor the <em>SLG solver</em> to work that way... hmm.....</p>



<a name="194683106"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/194683106" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#194683106">(Apr 20 2020 at 14:33)</a>:</h4>
<p>I remember thinking it should change, but I want to revisit my thoughts on that and see if I have a convincing reason why</p>



<a name="194683176"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/194683176" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#194683176">(Apr 20 2020 at 14:33)</a>:</h4>
<p>in any case, I could imagine that we setup something where chalk calls out to the rust-ir-database which (in turn) calls back into a "helper method" in chalk-solve, the main reason for the setup then being to enable salsa-style caching</p>



<a name="194683192"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/194683192" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#194683192">(Apr 20 2020 at 14:33)</a>:</h4>
<p>i.e., to intervene with a salsa query</p>



<a name="194683667"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/194683667" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Florian Diebold <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#194683667">(Apr 20 2020 at 14:36)</a>:</h4>
<p>yeah, that would basically be the idea for the recursive solver as well, right? except there cycles pose a problem</p>



<a name="194853216"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/194853216" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#194853216">(Apr 21 2020 at 19:56)</a>:</h4>
<p>Right, but they shouldn't if we extend salsa to permit cycles</p>



<a name="194853221"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/194853221" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#194853221">(Apr 21 2020 at 19:56)</a>:</h4>
<p>at least in cases like this</p>



<a name="194853233"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/recursive%20solver/near/194853233" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/recursive.20solver.html#194853233">(Apr 21 2020 at 19:56)</a>:</h4>
<p>which is what I wanted to talk to you about yesterday but didn't have time :( :(</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>